S, V:Type, M:(IdLnkIdType), l:IdLnk, s:S, v:V, L:((t:Id  (SV(M(l,t) List))) List).
tagged-messages(l;s;v;L)  ({m:Msg(M)| mlnk(m) = l}  List) 

latex

Definitions	x:A. B(x), x(s1,s2), t  T, Msg(M), tagged-messages(l;s;v;L), x. t(x), mlnk(m), t.1, x(s)
Lemmas	map wf, Msg wf, mlnk wf, tagged-list-messages wf, Id wf, IdLnk wf, pi1 wf